Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:	(neg(x) - neg(x)) - (neg(y) - neg(y))	→ (x - y) - (x - y)

There are 2 dependency pairs:


2:	(neg(x) - neg(x)) -# (neg(y) - neg(y))	→ (x - y) -# (x - y)
3:	(neg(x) - neg(x)) -# (neg(y) - neg(y))	→ x -# y

Consider the SCC {2,3}. By taking the AF π with π(-) = π(-#) = 1 together with the lexicographic path order with empty precedence, the rules in {1-3} are strictly decreasing. Hence the TRS is terminating.

Tyrolean Termination Tool (0.03 seconds) --- May 3, 2006